es:ES, e':E. hasloc(kind(e');loc(e')) 

latex

Definitions	t  T, P  Q, x:A. B(x), {T}, P & Q, P  Q, P  Q, Prop
Lemmas	event system wf, es-E wf, isrcv wf, assert wf, tagof wf, lnk wf, es-loc-rcv, es-kind wf, es-loc wf, assert-hasloc